# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

theory THEORY_DATATYPES ::cvc5::internal::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
typechecker "theory/datatypes/theory_datatypes_type_rules.h"

properties check parametric

rewriter ::cvc5::internal::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h"

# constructor type has a list of selector types followed by a return type
operator CONSTRUCTOR_TYPE 1: "constructor"
cardinality CONSTRUCTOR_TYPE \
    "::cvc5::internal::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \
    "theory/datatypes/theory_datatypes_type_rules.h"

# selector type has domain type and a range type
operator SELECTOR_TYPE 2 "selector"
# can re-use function cardinality
cardinality SELECTOR_TYPE \
    "::cvc5::internal::theory::uf::FunctionProperties::computeCardinality(%TYPE%)" \
    "theory/uf/theory_uf_type_rules.h"

# tester type has a constructor type
operator TESTER_TYPE 1 "tester"
# can re-use function cardinality
cardinality TESTER_TYPE \
    "::cvc5::internal::theory::uf::FunctionProperties::computeCardinality(%TYPE%)" \
    "theory/uf/theory_uf_type_rules.h"

# tester type has a constructor type
operator UPDATER_TYPE 2 "datatype update"
# can re-use function cardinality
cardinality UPDATER_TYPE \
    "::cvc5::internal::theory::uf::FunctionProperties::computeCardinality(%TYPE%)" \
    "theory/uf/theory_uf_type_rules.h"

parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor"

parameterized APPLY_SELECTOR SELECTOR_TYPE 1 "selector application; parameter is a datatype term (undefined if mis-applied)"

parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term"

parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with"

variable DATATYPE_TYPE
cardinality DATATYPE_TYPE \
    "%TYPE%.getDType().getCardinality(%TYPE%)" \
    "expr/dtype.h"
well-founded DATATYPE_TYPE \
    "%TYPE%.getDType().isWellFounded()" \
    "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
    "expr/dtype.h"

enumerator DATATYPE_TYPE \
    "::cvc5::internal::theory::datatypes::DatatypesEnumerator" \
    "theory/datatypes/type_enumerator.h"

operator PARAMETRIC_DATATYPE 1: "parametric datatype"
cardinality PARAMETRIC_DATATYPE \
    "%TYPE%.getDType().getCardinality(%TYPE%)" \
    "expr/dtype.h"
well-founded PARAMETRIC_DATATYPE \
    "%TYPE%.getDType().isWellFounded()" \
    "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
    "expr/dtype.h"

enumerator PARAMETRIC_DATATYPE \
    "::cvc5::internal::theory::datatypes::DatatypesEnumerator" \
    "theory/datatypes/type_enumerator.h"

operator TUPLE_TYPE 0: "tuple type"
cardinality TUPLE_TYPE \
    "%TYPE%.getDType().getCardinality(%TYPE%)" \
    "expr/dtype.h"
well-founded TUPLE_TYPE \
    "%TYPE%.getDType().isWellFounded()" \
    "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
    "expr/dtype.h"

enumerator TUPLE_TYPE \
    "::cvc5::internal::theory::datatypes::DatatypesEnumerator" \
    "expr/dtype.h"

parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
    "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed"
constant ASCRIPTION_TYPE \
  class \
  AscriptionType \
  ::cvc5::internal::AscriptionTypeHashFunction \
  "expr/ascription_type.h" \
  "a type parameter for type ascription; payload is an instance of the cvc5::internal::AscriptionType class"

typerule APPLY_CONSTRUCTOR ::cvc5::internal::theory::datatypes::DatatypeConstructorTypeRule
typerule APPLY_SELECTOR ::cvc5::internal::theory::datatypes::DatatypeSelectorTypeRule
typerule APPLY_TESTER ::cvc5::internal::theory::datatypes::DatatypeTesterTypeRule
typerule APPLY_UPDATER ::cvc5::internal::theory::datatypes::DatatypeUpdateTypeRule
typerule APPLY_TYPE_ASCRIPTION ::cvc5::internal::theory::datatypes::DatatypeAscriptionTypeRule
typerule ASCRIPTION_TYPE "SimpleTypeRule<RBuiltinOperator>"

# constructor applications are constant if they are applied only to constants
construle APPLY_CONSTRUCTOR ::cvc5::internal::theory::datatypes::DatatypeConstructorTypeRule

# the remaining kinds are used only by the sygus extension
operator DT_SIZE 1 "datatypes size"
typerule DT_SIZE ::cvc5::internal::theory::datatypes::DtSizeTypeRule

operator DT_HEIGHT_BOUND 2 "datatypes height bound"
typerule DT_HEIGHT_BOUND ::cvc5::internal::theory::datatypes::DtBoundTypeRule

operator DT_SIZE_BOUND 2 "datatypes height bound"
typerule DT_SIZE_BOUND ::cvc5::internal::theory::datatypes::DtBoundTypeRule

operator DT_SYGUS_BOUND 2 "datatypes sygus bound"
typerule DT_SYGUS_BOUND ::cvc5::internal::theory::datatypes::DtBoundTypeRule

operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function"
typerule DT_SYGUS_EVAL ::cvc5::internal::theory::datatypes::DtSygusEvalTypeRule


# Kinds for match terms. For example, the match term
#   (match l (((cons h t) h) (nil 0))) 
# is represented by the AST
#   (MATCH l 
#      (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h)
#      (MATCH_CASE nil 0)
#   )
# where notice that patterns with free variables use MATCH_BIND_CASE whereas
# patterns with no free variables use MATCH_CASE.

operator MATCH 2: "match construct"
operator MATCH_CASE 2 "a match case"
operator MATCH_BIND_CASE 3 "a match case with bound variables"

typerule MATCH ::cvc5::internal::theory::datatypes::MatchTypeRule
typerule MATCH_CASE ::cvc5::internal::theory::datatypes::MatchCaseTypeRule
typerule MATCH_BIND_CASE ::cvc5::internal::theory::datatypes::MatchBindCaseTypeRule


constant TUPLE_PROJECT_OP \
  class \
  ProjectOp+ \
  ::cvc5::internal::ProjectOpHashFunction \
  "theory/datatypes/project_op.h" \
  "operator for TUPLE_PROJECT; payload is an instance of the cvc5::internal::ProjectOp class"

parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \
    "projects a tuple from an existing tuple using indices passed in TupleProjectOp"

typerule TUPLE_PROJECT_OP  "SimpleTypeRule<RBuiltinOperator>"
typerule TUPLE_PROJECT     ::cvc5::internal::theory::datatypes::TupleProjectTypeRule

# For representing codatatype values
constant CODATATYPE_BOUND_VARIABLE \
    class \
    CodatatypeBoundVariable \
    ::cvc5::internal::CodatatypeBoundVariableHashFunction \
    "expr/codatatype_bound_variable.h" \
    "the kind of expressions representing bound variables in codatatype constants, which are de Bruijn indexed variables; payload is an instance of the cvc5::internal::CodatatypeBoundVariable class (used in models)"
typerule CODATATYPE_BOUND_VARIABLE ::cvc5::internal::theory::datatypes::CodatatypeBoundVariableTypeRule


operator NULLABLE_TYPE 0: "nullable type"
cardinality NULLABLE_TYPE \
    "%TYPE%.getDType().getCardinality(%TYPE%)" \
    "expr/dtype.h"
well-founded NULLABLE_TYPE \
    "%TYPE%.getDType().isWellFounded()" \
    "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
    "expr/dtype.h"

enumerator NULLABLE_TYPE \
    "::cvc5::internal::theory::datatypes::DatatypesEnumerator" \
    "expr/dtype.h"

operator NULLABLE_LIFT  1: "application of lift operator; first parameter is the lift operator, remaining ones are its arguments"

typerule NULLABLE_LIFT          ::cvc5::internal::theory::datatypes::NullableLiftTypeRule

endtheory
